Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		from(X)	→ cons(X,n__from(n__s(X)))
2:		after(0,XS)	→ XS
3:		after(s(N),cons(X,XS))	→ after(N,activate(XS))
4:		from(X)	→ n__from(X)
5:		s(X)	→ n__s(X)
6:		activate(n__from(X))	→ from(activate(X))
7:		activate(n__s(X))	→ s(activate(X))
8:		activate(X)	→ X

There are 6 dependency pairs:


9:		AFTER(s(N),cons(X,XS))	→ AFTER(N,activate(XS))
10:		AFTER(s(N),cons(X,XS))	→ ACTIVATE(XS)
11:		ACTIVATE(n__from(X))	→ FROM(activate(X))
12:		ACTIVATE(n__from(X))	→ ACTIVATE(X)
13:		ACTIVATE(n__s(X))	→ S(activate(X))
14:		ACTIVATE(n__s(X))	→ ACTIVATE(X)

The approximated dependency graph contains 2 SCCs: {12,14} and {9}.

Consider the SCC {12,14}. There are no usable rules. By taking the AF π with π(ACTIVATE) = π(n__from) = 1 together with the lexicographic path order with empty precedence, rule 12 is weakly decreasing and rule 14 is strictly decreasing. There is one new SCC.
- Consider the SCC {12}. By taking the AF π with π(ACTIVATE) = 1 together with the lexicographic path order with empty precedence, rule 12 is strictly decreasing.

Consider the SCC {9}. The usable rules are {1,4-8}. By taking the AF π with π(AFTER) = π(cons) = π(from) = π(n__from) = 1 together with the lexicographic path order with precedence activate ≻ s ≻ n__s, the rules in {1,4,6} are weakly decreasing and the rules in {5,7-9} are strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (0.05 seconds) --- May 3, 2006